The present application relates to checking properties of bounded concurrent programs using a staged data-centric analysis.
Analyzing shared memory concurrent programs is difficult due to the fact that constituent program threads may interfere with each other via shared variables. Multiple formalisms have been developed to model and reason about interference, e.g., the Mazurkiewicz traces model the program behaviors as a partial order over events while the context-switching model utilizes a scheduler to generate all possible thread interleavings. Because analyzing all possible interferences is intractable in practice, these models employ reduction techniques to focus on a subset of interferences, e.g., partial-order reduction or context-bounding. Both M-traces and context-switching are control-centric formalisms, i.e., data flow among concurrent threads is induced by enforcing causal orders between concurrent events directly or by explicitly switching control between threads.
Recent approaches have employed a different approach for verification based on memory consistency (MC) models, which prescribe rules on which write a read may observe in a valid program execution. An MC model is data-centric, i.e., the causal order between concurrent events is determined based on the data flow from writes to reads. The MC formalism is attractive for program verification because it allows reasoning about concurrent read-write interference directly while retaining the partial orders among events. The most well-known and intuitive model is that of sequential consistency (SC), where all concurrent threads observe the same global order of events and each read observes the most recent write. In spite of the ubiquitous presence of SC in concurrent program analysis, the logical foundations of SC have received little attention besides, where various MC models are formalized in higher-order logic uniformly.
FIG. 1 shows a prior art system to check properties of concurrent programs. The system of FIG. 1 encodes the individual threads of the concurrent control flow graph and the property of the program as formula F1 (10). The encoding includes the existence of potential bugs as part of the property. Next the system encodes the interactions between program threads (interference) as formula F2 (12). The system checks to see if the conjunction between formulas F1 and F2 (F1^F2) is satisfied (14). In 16, if yes, the system provides a witness to enable a user to recreate the bug or problem. Alternatively, if there is no bug, the system generates the proof that the program is correct and bug-free.
Even with the system of FIG. 1, checking properties of bounded concurrent C programs automatically using symbolic methods is difficult due to large number of possible interleavings of concurrent programs that the analysis must explore.